(set-logic QF_LRA)
(set-info :source |
The Formal Verification of a Reintegration Protocol. Author: Lee Pike. Website: http://www.cs.indiana.edu/~lepike/pub_pages/emsoft.html.

This benchmark was automatically translated into SMT-LIB format from
CVC format using CVC Lite
|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun x_0 () Real)
(declare-fun x_1 () Real)
(declare-fun x_2 () Bool)
(declare-fun x_3 () Bool)
(declare-fun x_4 () Bool)
(declare-fun x_5 () Bool)
(declare-fun x_6 () Real)
(declare-fun x_7 () Real)
(declare-fun x_8 () Real)
(declare-fun x_9 () Real)
(declare-fun x_10 () Real)
(declare-fun x_11 () Real)
(declare-fun x_12 () Bool)
(declare-fun x_13 () Bool)
(declare-fun x_14 () Bool)
(declare-fun x_15 () Bool)
(declare-fun x_16 () Bool)
(declare-fun x_17 () Bool)
(declare-fun x_18 () Bool)
(declare-fun x_19 () Bool)
(declare-fun x_20 () Real)
(declare-fun x_21 () Real)
(declare-fun x_22 () Real)
(declare-fun x_23 () Bool)
(declare-fun x_24 () Real)
(declare-fun x_25 () Real)
(declare-fun x_26 () Real)
(declare-fun x_27 () Real)
(declare-fun x_28 () Bool)
(declare-fun x_29 () Real)
(declare-fun x_30 () Bool)
(declare-fun x_31 () Bool)
(declare-fun x_32 () Bool)
(declare-fun x_33 () Bool)
(declare-fun x_34 () Bool)
(declare-fun x_35 () Bool)
(declare-fun x_36 () Real)
(declare-fun x_37 () Real)
(declare-fun x_38 () Real)
(declare-fun x_39 () Real)
(declare-fun x_40 () Bool)
(declare-fun x_41 () Bool)
(declare-fun x_42 () Bool)
(declare-fun x_43 () Bool)
(declare-fun x_44 () Bool)
(declare-fun x_45 () Real)
(declare-fun x_46 () Real)
(declare-fun x_47 () Real)
(declare-fun x_48 () Real)
(declare-fun x_49 () Real)
(declare-fun x_50 () Real)
(declare-fun x_51 () Real)
(declare-fun x_52 () Real)
(declare-fun x_53 () Real)
(declare-fun x_54 () Bool)
(declare-fun x_55 () Real)
(declare-fun x_56 () Real)
(declare-fun x_57 () Real)
(declare-fun x_58 () Real)
(declare-fun x_59 () Bool)
(declare-fun x_60 () Real)
(declare-fun x_61 () Bool)
(declare-fun x_62 () Bool)
(declare-fun x_63 () Bool)
(declare-fun x_64 () Bool)
(declare-fun x_65 () Bool)
(declare-fun x_66 () Bool)
(declare-fun x_67 () Real)
(declare-fun x_68 () Real)
(declare-fun x_69 () Real)
(declare-fun x_70 () Real)
(declare-fun x_71 () Bool)
(declare-fun x_72 () Bool)
(declare-fun x_73 () Bool)
(declare-fun x_74 () Bool)
(declare-fun x_75 () Bool)
(declare-fun x_76 () Real)
(declare-fun x_77 () Real)
(declare-fun x_78 () Real)
(declare-fun x_79 () Real)
(declare-fun x_80 () Real)
(declare-fun x_81 () Real)
(declare-fun x_82 () Real)
(declare-fun x_83 () Real)
(declare-fun x_84 () Real)
(declare-fun x_85 () Bool)
(declare-fun x_86 () Real)
(declare-fun x_87 () Real)
(declare-fun x_88 () Real)
(declare-fun x_89 () Real)
(declare-fun x_90 () Bool)
(declare-fun x_91 () Real)
(declare-fun x_92 () Bool)
(declare-fun x_93 () Bool)
(declare-fun x_94 () Bool)
(declare-fun x_95 () Bool)
(declare-fun x_96 () Bool)
(declare-fun x_97 () Bool)
(declare-fun x_98 () Real)
(declare-fun x_99 () Real)
(declare-fun x_100 () Real)
(declare-fun x_101 () Real)
(declare-fun x_102 () Bool)
(declare-fun x_103 () Bool)
(declare-fun x_104 () Bool)
(declare-fun x_105 () Bool)
(declare-fun x_106 () Bool)
(declare-fun x_107 () Real)
(declare-fun x_108 () Real)
(declare-fun x_109 () Real)
(declare-fun x_110 () Real)
(declare-fun x_111 () Real)
(declare-fun x_112 () Real)
(declare-fun x_113 () Real)
(declare-fun x_114 () Real)
(declare-fun x_115 () Real)
(declare-fun x_116 () Bool)
(declare-fun x_117 () Real)
(declare-fun x_118 () Real)
(declare-fun x_119 () Real)
(declare-fun x_120 () Real)
(declare-fun x_121 () Bool)
(declare-fun x_122 () Real)
(declare-fun x_123 () Bool)
(declare-fun x_124 () Bool)
(declare-fun x_125 () Bool)
(declare-fun x_126 () Bool)
(declare-fun x_127 () Bool)
(declare-fun x_128 () Bool)
(declare-fun x_129 () Real)
(declare-fun x_130 () Real)
(declare-fun x_131 () Real)
(declare-fun x_132 () Real)
(declare-fun x_133 () Bool)
(declare-fun x_134 () Bool)
(declare-fun x_135 () Bool)
(declare-fun x_136 () Bool)
(declare-fun x_137 () Bool)
(declare-fun x_138 () Real)
(declare-fun x_139 () Real)
(declare-fun x_140 () Real)
(declare-fun x_141 () Real)
(declare-fun x_142 () Real)
(declare-fun x_143 () Real)
(declare-fun x_144 () Real)
(declare-fun x_145 () Real)
(declare-fun x_146 () Real)
(declare-fun x_147 () Bool)
(declare-fun x_148 () Real)
(declare-fun x_149 () Real)
(declare-fun x_150 () Real)
(assert (let ((?v_3 (- x_0 x_1)) (?v_241 (+ x_1 x_9)) (?v_284 (<= x_0 x_27)) (?v_264 (= x_28 x_16)) (?v_214 (= x_29 0)) (?v_227 (< x_0 x_11)) (?v_249 (= x_27 x_0)) (?v_274 (= x_29 2)) (?v_276 (= x_30 x_5)) (?v_277 (and (= x_31 x_3) (= x_32 x_4))) (?v_262 (= x_33 x_19)) (?v_263 (and (= x_34 x_17) (= x_35 x_18))) (?v_278 (= x_36 x_8)) (?v_279 (and (= x_37 x_6) (= x_38 x_7))) (?v_236 (= x_39 x_11)) (?v_261 (= x_40 x_2)) (?v_259 (= x_41 x_15)) (?v_260 (and (= x_42 x_13) (= x_43 x_14))) (?v_280 (= x_44 x_12)) (?v_285 (- x_45 x_1)) (?v_215 (= x_29 1)) (?v_256 (+ x_9 x_1)) (?v_252 (<= x_24 x_27))) (let ((?v_258 (= x_30 (or x_5 (and ?v_252 x_15)))) (?v_245 (<= x_21 ?v_241)) (?v_247 (<= x_22 ?v_241)) (?v_244 (<= x_21 x_9)) (?v_246 (<= x_22 x_9)) (?v_221 (not x_3)) (?v_266 (< x_21 x_0)) (?v_267 (= x_27 x_21)) (?v_222 (not x_4)) (?v_269 (< x_22 x_0)) (?v_270 (= x_27 x_22)) (?v_223 (not x_5)) (?v_286 (not ?v_284)) (?v_238 (not x_13)) (?v_240 (not x_14)) (?v_242 (not x_15))) (let ((?v_237 (not ?v_244))) (let ((?v_250 (and ?v_237 (<= x_21 x_27))) (?v_239 (not ?v_246))) (let ((?v_251 (and ?v_239 (<= x_22 x_27)))) (let ((?v_257 (and (= x_31 (or x_3 (and ?v_250 x_13))) (= x_32 (or x_4 (and ?v_251 x_14))))) (?v_248 (<= x_24 ?v_241)) (?v_272 (< x_24 x_0)) (?v_273 (= x_27 x_24)) (?v_253 (not ?v_245)) (?v_254 (not ?v_247)) (?v_4 (not (<= x_24 x_9)))) (let ((?v_7 (and ?v_4 ?v_252)) (?v_6 (not (<= x_25 x_9)))) (let ((?v_8 (and ?v_6 (<= x_25 x_27))) (?v_255 (not ?v_248)) (?v_175 (+ x_1 x_27)) (?v_216 (<= x_45 x_58)) (?v_200 (= x_59 x_28)) (?v_150 (= x_60 0)) (?v_160 (< x_45 x_39)) (?v_185 (= x_58 x_45)) (?v_207 (= x_60 2)) (?v_209 (= x_61 x_30)) (?v_210 (and (= x_62 x_31) (= x_63 x_32))) (?v_198 (= x_64 x_33)) (?v_199 (and (= x_65 x_34) (= x_66 x_35))) (?v_211 (= x_67 x_36)) (?v_212 (and (= x_68 x_37) (= x_69 x_38))) (?v_170 (= x_70 x_39)) (?v_197 (= x_71 x_40)) (?v_195 (= x_72 x_41)) (?v_196 (and (= x_73 x_42) (= x_74 x_43))) (?v_213 (= x_75 x_44)) (?v_217 (- x_76 x_1)) (?v_151 (= x_60 1)) (?v_192 (+ x_27 x_1)) (?v_188 (<= x_55 x_58))) (let ((?v_194 (= x_61 (or x_30 (and ?v_188 x_41)))) (?v_178 (<= x_52 ?v_175)) (?v_180 (<= x_53 ?v_175)) (?v_177 (<= x_52 x_27)) (?v_179 (<= x_53 x_27)) (?v_172 (not x_31)) (?v_201 (< x_52 x_45)) (?v_202 (= x_58 x_52)) (?v_174 (not x_32)) (?v_203 (< x_53 x_45)) (?v_204 (= x_58 x_53)) (?v_163 (not x_30)) (?v_218 (not ?v_216)) (?v_182 (not x_42)) (?v_183 (not x_43)) (?v_184 (not x_41))) (let ((?v_171 (not ?v_177))) (let ((?v_186 (and ?v_171 (<= x_52 x_58))) (?v_173 (not ?v_179))) (let ((?v_187 (and ?v_173 (<= x_53 x_58)))) (let ((?v_193 (and (= x_62 (or x_31 (and ?v_186 x_42))) (= x_63 (or x_32 (and ?v_187 x_43))))) (?v_181 (<= x_55 ?v_175)) (?v_205 (< x_55 x_45)) (?v_206 (= x_58 x_55)) (?v_189 (not ?v_178)) (?v_190 (not ?v_180)) (?v_287 (not (<= x_55 x_27)))) (let ((?v_13 (and ?v_287 ?v_188)) (?v_288 (not (<= x_56 x_27)))) (let ((?v_14 (and ?v_288 (<= x_56 x_58))) (?v_191 (not ?v_181)) (?v_111 (+ x_1 x_58)) (?v_152 (<= x_76 x_89)) (?v_136 (= x_90 x_59)) (?v_88 (= x_91 0)) (?v_96 (< x_76 x_70)) (?v_121 (= x_89 x_76)) (?v_143 (= x_91 2)) (?v_145 (= x_92 x_61)) (?v_146 (and (= x_93 x_62) (= x_94 x_63))) (?v_134 (= x_95 x_64)) (?v_135 (and (= x_96 x_65) (= x_97 x_66))) (?v_147 (= x_98 x_67)) (?v_148 (and (= x_99 x_68) (= x_100 x_69))) (?v_106 (= x_101 x_70)) (?v_133 (= x_102 x_71)) (?v_131 (= x_103 x_72)) (?v_132 (and (= x_104 x_73) (= x_105 x_74))) (?v_149 (= x_106 x_75)) (?v_153 (- x_107 x_1)) (?v_89 (= x_91 1)) (?v_128 (+ x_58 x_1)) (?v_124 (<= x_86 x_89))) (let ((?v_130 (= x_92 (or x_61 (and ?v_124 x_72)))) (?v_114 (<= x_83 ?v_111)) (?v_116 (<= x_84 ?v_111)) (?v_113 (<= x_83 x_58)) (?v_115 (<= x_84 x_58)) (?v_108 (not x_62)) (?v_137 (< x_83 x_76)) (?v_138 (= x_89 x_83)) (?v_110 (not x_63)) (?v_139 (< x_84 x_76)) (?v_140 (= x_89 x_84)) (?v_99 (not x_61)) (?v_154 (not ?v_152)) (?v_118 (not x_73)) (?v_119 (not x_74)) (?v_120 (not x_72))) (let ((?v_107 (not ?v_113))) (let ((?v_122 (and ?v_107 (<= x_83 x_89))) (?v_109 (not ?v_115))) (let ((?v_123 (and ?v_109 (<= x_84 x_89)))) (let ((?v_129 (and (= x_93 (or x_62 (and ?v_122 x_73))) (= x_94 (or x_63 (and ?v_123 x_74))))) (?v_117 (<= x_86 ?v_111)) (?v_141 (< x_86 x_76)) (?v_142 (= x_89 x_86)) (?v_125 (not ?v_114)) (?v_126 (not ?v_116)) (?v_219 (not (<= x_86 x_58)))) (let ((?v_19 (and ?v_219 ?v_124)) (?v_220 (not (<= x_87 x_58)))) (let ((?v_20 (and ?v_220 (<= x_87 x_89))) (?v_127 (not ?v_117)) (?v_49 (+ x_1 x_89)) (?v_90 (<= x_107 x_120)) (?v_74 (= x_121 x_90)) (?v_33 (= x_122 0)) (?v_34 (< x_107 x_101)) (?v_58 (= x_120 x_107)) (?v_81 (= x_122 2)) (?v_83 (= x_123 x_92)) (?v_84 (and (= x_124 x_93) (= x_125 x_94))) (?v_72 (= x_126 x_95)) (?v_73 (and (= x_127 x_96) (= x_128 x_97))) (?v_85 (= x_129 x_98)) (?v_86 (and (= x_130 x_99) (= x_131 x_100))) (?v_44 (= x_132 x_101)) (?v_71 (= x_133 x_102)) (?v_69 (= x_134 x_103)) (?v_70 (and (= x_135 x_104) (= x_136 x_105))) (?v_87 (= x_137 x_106)) (?v_91 (- x_138 x_1)) (?v_62 (= x_122 1)) (?v_66 (+ x_89 x_1)) (?v_61 (<= x_117 x_120))) (let ((?v_68 (= x_123 (or x_92 (and ?v_61 x_103)))) (?v_51 (<= x_114 ?v_49)) (?v_53 (<= x_115 ?v_49)) (?v_50 (<= x_114 x_89)) (?v_52 (<= x_115 x_89)) (?v_46 (not x_93)) (?v_75 (< x_114 x_107)) (?v_76 (= x_120 x_114)) (?v_48 (not x_94)) (?v_77 (< x_115 x_107)) (?v_78 (= x_120 x_115)) (?v_37 (not x_92)) (?v_92 (not ?v_90)) (?v_55 (not x_104)) (?v_56 (not x_105)) (?v_57 (not x_103))) (let ((?v_45 (not ?v_50))) (let ((?v_59 (and ?v_45 (<= x_114 x_120))) (?v_47 (not ?v_52))) (let ((?v_60 (and ?v_47 (<= x_115 x_120)))) (let ((?v_67 (and (= x_124 (or x_93 (and ?v_59 x_104))) (= x_125 (or x_94 (and ?v_60 x_105))))) (?v_54 (<= x_117 ?v_49)) (?v_79 (< x_117 x_107)) (?v_80 (= x_120 x_117)) (?v_63 (not ?v_51)) (?v_64 (not ?v_53)) (?v_155 (not (<= x_117 x_89)))) (let ((?v_25 (and ?v_155 ?v_61)) (?v_156 (not (<= x_118 x_89)))) (let ((?v_26 (and ?v_156 (<= x_118 x_120))) (?v_65 (not ?v_54)) (?v_0 (= x_6 0)) (?v_1 (= x_7 0)) (?v_2 (= x_8 0)) (?v_235 (= x_36 0)) (?v_226 (= x_36 3)) (?v_231 (= x_37 0)) (?v_224 (= x_37 3)) (?v_233 (= x_38 0)) (?v_225 (= x_38 3)) (?v_169 (= x_67 0)) (?v_159 (= x_67 3)) (?v_165 (= x_68 0)) (?v_157 (= x_68 3)) (?v_167 (= x_69 0)) (?v_158 (= x_69 3)) (?v_105 (= x_98 0)) (?v_95 (= x_98 3)) (?v_101 (= x_99 0)) (?v_93 (= x_99 3)) (?v_103 (= x_100 0)) (?v_94 (= x_100 3)) (?v_43 (= x_129 0)) (?v_32 (= x_129 3)) (?v_39 (= x_130 0)) (?v_30 (= x_130 3)) (?v_41 (= x_131 0)) (?v_31 (= x_131 3)) (?v_282 (not x_2)) (?v_265 (not x_17)) (?v_268 (not x_18)) (?v_271 (not x_19)) (?v_281 (= x_20 0)) (?v_9 (and (not (<= x_26 x_9)) (<= x_26 x_27))) (?v_15 (and (not (<= x_57 x_27)) (<= x_57 x_58))) (?v_21 (and (not (<= x_88 x_58)) (<= x_88 x_89))) (?v_27 (and (not (<= x_119 x_89)) (<= x_119 x_120))) (?v_35 (= x_130 (ite ?v_46 (ite (and ?v_59 (< x_99 3)) (+ x_99 1) x_99) x_99))) (?v_36 (= x_131 (ite ?v_48 (ite (and ?v_60 (< x_100 3)) (+ x_100 1) x_100) x_100)))) (let ((?v_38 (or x_93 ?v_30)) (?v_40 (or x_94 ?v_31)) (?v_42 (or x_92 ?v_32)) (?v_112 (not x_106)) (?v_97 (= x_99 (ite ?v_108 (ite (and ?v_122 (< x_68 3)) (+ x_68 1) x_68) x_68))) (?v_98 (= x_100 (ite ?v_110 (ite (and ?v_123 (< x_69 3)) (+ x_69 1) x_69) x_69))) (?v_100 (or x_62 ?v_93)) (?v_102 (or x_63 ?v_94)) (?v_104 (or x_61 ?v_95)) (?v_176 (not x_75)) (?v_161 (= x_68 (ite ?v_172 (ite (and ?v_186 (< x_37 3)) (+ x_37 1) x_37) x_37))) (?v_162 (= x_69 (ite ?v_174 (ite (and ?v_187 (< x_38 3)) (+ x_38 1) x_38) x_38))) (?v_164 (or x_31 ?v_157)) (?v_166 (or x_32 ?v_158)) (?v_168 (or x_30 ?v_159)) (?v_243 (not x_44)) (?v_228 (= x_37 (ite ?v_221 (ite (and ?v_250 (< x_6 3)) (+ x_6 1) x_6) x_6))) (?v_229 (= x_38 (ite ?v_222 (ite (and ?v_251 (< x_7 3)) (+ x_7 1) x_7) x_7))) (?v_230 (or x_3 ?v_224)) (?v_232 (or x_4 ?v_225)) (?v_234 (or x_5 ?v_226)) (?v_283 (= x_20 1)) (?v_5 (ite ?v_7 2 1)) (?v_10 (ite ?v_7 3 2)) (?v_11 (ite ?v_7 1 0)) (?v_12 (ite ?v_13 2 1)) (?v_16 (ite ?v_13 3 2)) (?v_17 (ite ?v_13 1 0)) (?v_18 (ite ?v_19 2 1)) (?v_22 (ite ?v_19 3 2)) (?v_23 (ite ?v_19 1 0)) (?v_24 (ite ?v_25 2 1)) (?v_28 (ite ?v_25 3 2)) (?v_29 (ite ?v_25 1 0)) (?v_82 (<= (ite x_95 (ite x_97 (ite x_96 3 2) x_139) (ite x_97 x_139 (ite x_96 1 0))) (* (* (ite x_92 (ite x_94 (ite x_93 0 1) x_140) (ite x_94 x_140 (ite x_93 2 3))) 1) (/ 1 2)))) (?v_144 (<= (ite x_64 (ite x_66 (ite x_65 3 2) x_108) (ite x_66 x_108 (ite x_65 1 0))) (* (* (ite x_61 (ite x_63 (ite x_62 0 1) x_109) (ite x_63 x_109 (ite x_62 2 3))) 1) (/ 1 2)))) (?v_208 (<= (ite x_33 (ite x_35 (ite x_34 3 2) x_77) (ite x_35 x_77 (ite x_34 1 0))) (* (* (ite x_30 (ite x_32 (ite x_31 0 1) x_78) (ite x_32 x_78 (ite x_31 2 3))) 1) (/ 1 2)))) (?v_275 (<= (ite x_19 (ite x_18 (ite x_17 3 2) x_46) (ite x_18 x_46 (ite x_17 1 0))) (* (* (ite x_5 (ite x_4 (ite x_3 0 1) x_47) (ite x_4 x_47 (ite x_3 2 3))) 1) (/ 1 2))))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (<= x_122 2) (>= x_122 0)) (<= x_91 2)) (>= x_91 0)) (<= x_60 2)) (>= x_60 0)) (<= x_29 2)) (>= x_29 0)) (<= x_20 2)) (>= x_20 0)) (>= x_0 0)) (> x_1 0)) (>= x_1 0)) (or (or (or ?v_0 (= x_6 1)) (= x_6 2)) (= x_6 3))) (not (< x_6 0))) (<= x_6 3)) (or (or (or ?v_1 (= x_7 1)) (= x_7 2)) (= x_7 3))) (not (< x_7 0))) (<= x_7 3)) (or (or (or ?v_2 (= x_8 1)) (= x_8 2)) (= x_8 3))) (not (< x_8 0))) (<= x_8 3)) (>= x_9 0)) (not (<= x_10 (* x_1 3)))) (>= x_10 0)) (>= x_11 0)) (>= x_21 0)) (>= x_22 0)) (>= x_24 0)) (>= x_25 0)) (>= x_26 0)) (>= x_27 0)) (or (or (or ?v_235 (= x_36 1)) (= x_36 2)) ?v_226)) (not (< x_36 0))) (<= x_36 3)) (or (or (or ?v_231 (= x_37 1)) (= x_37 2)) ?v_224)) (not (< x_37 0))) (<= x_37 3)) (or (or (or ?v_233 (= x_38 1)) (= x_38 2)) ?v_225)) (not (< x_38 0))) (<= x_38 3)) (>= x_39 0)) (>= x_45 0)) (>= x_52 0)) (>= x_53 0)) (>= x_55 0)) (>= x_56 0)) (>= x_57 0)) (>= x_58 0)) (or (or (or ?v_169 (= x_67 1)) (= x_67 2)) ?v_159)) (not (< x_67 0))) (<= x_67 3)) (or (or (or ?v_165 (= x_68 1)) (= x_68 2)) ?v_157)) (not (< x_68 0))) (<= x_68 3)) (or (or (or ?v_167 (= x_69 1)) (= x_69 2)) ?v_158)) (not (< x_69 0))) (<= x_69 3)) (>= x_70 0)) (>= x_76 0)) (>= x_83 0)) (>= x_84 0)) (>= x_86 0)) (>= x_87 0)) (>= x_88 0)) (>= x_89 0)) (or (or (or ?v_105 (= x_98 1)) (= x_98 2)) ?v_95)) (not (< x_98 0))) (<= x_98 3)) (or (or (or ?v_101 (= x_99 1)) (= x_99 2)) ?v_93)) (not (< x_99 0))) (<= x_99 3)) (or (or (or ?v_103 (= x_100 1)) (= x_100 2)) ?v_94)) (not (< x_100 0))) (<= x_100 3)) (>= x_101 0)) (>= x_107 0)) (>= x_114 0)) (>= x_115 0)) (>= x_117 0)) (>= x_118 0)) (>= x_119 0)) (>= x_120 0)) (or (or (or ?v_43 (= x_129 1)) (= x_129 2)) ?v_32)) (not (< x_129 0))) (<= x_129 3)) (or (or (or ?v_39 (= x_130 1)) (= x_130 2)) ?v_30)) (not (< x_130 0))) (<= x_130 3)) (or (or (or ?v_41 (= x_131 1)) (= x_131 2)) ?v_31)) (not (< x_131 0))) (<= x_131 3)) (>= x_132 0)) (>= x_138 0)) (>= x_145 0)) (>= x_146 0)) (>= x_148 0)) (>= x_149 0)) (>= x_150 0)) ?v_282) ?v_221) ?v_222) ?v_223) ?v_0) ?v_1) ?v_2) (not (< x_9 0))) (< x_9 x_10)) (= x_11 (+ (+ x_9 x_10) x_1))) x_12) ?v_238) ?v_240) ?v_242) x_16) ?v_265) ?v_268) ?v_271) ?v_281) (not (<= x_0 x_21))) (not (<= x_21 ?v_3))) (not (<= x_0 x_22))) (not (<= x_22 ?v_3))) (= x_0 (ite (not (< x_9 x_1)) (+ x_10 x_1) x_1))) (not x_23)) ?v_4) ?v_6) (< x_24 x_25)) (< x_25 x_26)) (= x_46 (ite x_17 2 1))) (= x_47 (ite x_3 1 2))) (= x_48 ?v_5)) (= x_49 ?v_5)) (= x_50 (+ (ite ?v_9 (ite ?v_8 ?v_10 x_48) (ite ?v_8 x_48 ?v_11)) x_8))) (= x_51 (+ (ite ?v_9 (ite ?v_8 ?v_10 x_49) (ite ?v_8 x_49 ?v_11)) x_8))) (= x_77 (ite x_34 2 1))) (= x_78 (ite x_31 1 2))) (= x_79 ?v_12)) (= x_80 ?v_12)) (= x_81 (+ (ite ?v_15 (ite ?v_14 ?v_16 x_79) (ite ?v_14 x_79 ?v_17)) x_36))) (= x_82 (+ (ite ?v_15 (ite ?v_14 ?v_16 x_80) (ite ?v_14 x_80 ?v_17)) x_36))) (= x_108 (ite x_65 2 1))) (= x_109 (ite x_62 1 2))) (= x_110 ?v_18)) (= x_111 ?v_18)) (= x_112 (+ (ite ?v_21 (ite ?v_20 ?v_22 x_110) (ite ?v_20 x_110 ?v_23)) x_67))) (= x_113 (+ (ite ?v_21 (ite ?v_20 ?v_22 x_111) (ite ?v_20 x_111 ?v_23)) x_67))) (= x_139 (ite x_96 2 1))) (= x_140 (ite x_93 1 2))) (= x_141 ?v_24)) (= x_142 ?v_24)) (= x_143 (+ (ite ?v_27 (ite ?v_26 ?v_28 x_141) (ite ?v_26 x_141 ?v_29)) x_98))) (= x_144 (+ (ite ?v_27 (ite ?v_26 ?v_28 x_142) (ite ?v_26 x_142 ?v_29)) x_98))) (or (or (and (and (and (and (and (and (or (and (and (and (and (and (and (and (and (and (and ?v_33 ?v_34) ?v_58) ?v_35) ?v_36) (= x_129 (ite ?v_37 (ite (not (< x_143 3)) 3 x_143) x_98))) (= x_124 ?v_38)) (= x_125 ?v_40)) (= x_123 ?v_42)) ?v_71) ?v_44) (and (and (and (and (and (and (and (and (and (and ?v_33 (not ?v_34)) x_133) (= x_120 x_101)) ?v_35) ?v_36) (= x_129 (ite ?v_37 (ite (not (< x_144 3)) 3 x_144) x_98))) (= x_124 (or ?v_38 ?v_39))) (= x_125 (or ?v_40 ?v_41))) (= x_123 (or ?v_42 ?v_43))) ?v_44)) ?v_69) ?v_70) ?v_87) ?v_72) ?v_73) ?v_74) (and (and (and (and (and (and (and (or (and (and (and (and (and (and (and (and (and (and (and ?v_62 (or (or (and (and (and ?v_45 ?v_46) ?v_55) ?v_51) (and (and (and ?v_47 ?v_48) ?v_56) ?v_53)) (and (and ?v_37 ?v_57) ?v_54))) (not x_137)) (or (or (or (or ?v_50 ?v_63) x_104) x_93) (not (< x_120 x_114)))) (or (or (or (or ?v_52 ?v_64) x_105) x_94) (not (< x_120 x_115)))) (or (or (or ?v_65 x_103) x_92) (not (< x_120 x_117)))) (or (or (or (and (and (and (and ?v_55 ?v_46) ?v_51) ?v_75) ?v_76) (and (and (and (and ?v_56 ?v_48) ?v_53) ?v_77) ?v_78)) (and (and (and (and ?v_57 ?v_37) ?v_54) ?v_79) ?v_80)) (and (< x_107 ?v_66) ?v_58))) (= x_135 (or x_104 ?v_59))) (= x_136 (or x_105 ?v_60))) (= x_134 (or x_103 ?v_61))) ?v_67) ?v_68) (and (and (and (and (and (and (and (and (and ?v_62 (or (or (or ?v_50 x_104) x_93) ?v_63)) (or (or (or ?v_52 x_105) x_94) ?v_64)) (or (or x_103 x_92) ?v_65)) x_137) (= x_120 ?v_66)) ?v_67) ?v_68) ?v_69) ?v_70)) ?v_85) ?v_86) ?v_44) ?v_71) ?v_72) ?v_73) ?v_74)) (and (and (and (and (and (and (and (or (and (and (and (and (and (and (and (and (and (and (and ?v_81 ?v_82) (not x_121)) (or (or (or ?v_50 x_96) x_93) (<= x_120 x_114))) (or (or (or ?v_52 x_97) x_94) (<= x_120 x_115))) (or (or x_95 x_92) (<= x_120 x_117))) (or (or (or (and (and (and (and (not x_96) ?v_46) (< x_89 x_114)) ?v_75) ?v_76) (and (and (and (and (not x_97) ?v_48) (< x_89 x_115)) ?v_77) ?v_78)) (and (and (and (not x_95) ?v_37) ?v_79) ?v_80)) ?v_58)) (= x_127 (or x_96 (= x_114 x_120)))) (= x_128 (or x_97 (= x_115 x_120)))) (= x_126 (or x_95 (= x_117 x_120)))) ?v_83) ?v_84) (and (and (and (and (and (and (and ?v_81 (not ?v_82)) x_121) ?v_83) ?v_84) (= x_120 x_89)) ?v_72) ?v_73)) ?v_85) ?v_86) ?v_44) ?v_71) ?v_69) ?v_70) ?v_87))) (or (or (and ?v_88 (= x_122 (ite (not x_102) x_91 1))) (and ?v_89 (= x_122 (ite ?v_112 x_91 2)))) (and (and (not ?v_88) (not ?v_89)) (= x_122 x_91)))) (or (and (and ?v_90 (not (<= x_138 x_145))) (not (<= x_145 ?v_91))) (and ?v_92 (= x_145 x_114)))) (or (and (and ?v_90 (not (<= x_138 x_146))) (not (<= x_146 ?v_91))) (and ?v_92 (= x_146 x_115)))) (or (and (and ?v_90 (= x_138 (+ x_107 x_10))) x_147) (and (and ?v_92 (not x_147)) (= x_138 x_107)))) (or (and (and (and (and ?v_61 (not (<= x_148 x_120))) (not (<= x_149 x_120))) (< x_148 x_149)) (< x_149 x_150)) (and (and (and (not ?v_61) (= x_148 x_117)) (= x_149 x_118)) (= x_150 x_119)))) (or (or (and (and (and (and (and (and (or (and (and (and (and (and (and (and (and (and (and ?v_88 ?v_96) ?v_121) ?v_97) ?v_98) (= x_98 (ite ?v_99 (ite (not (< x_112 3)) 3 x_112) x_67))) (= x_93 ?v_100)) (= x_94 ?v_102)) (= x_92 ?v_104)) ?v_133) ?v_106) (and (and (and (and (and (and (and (and (and (and ?v_88 (not ?v_96)) x_102) (= x_89 x_70)) ?v_97) ?v_98) (= x_98 (ite ?v_99 (ite (not (< x_113 3)) 3 x_113) x_67))) (= x_93 (or ?v_100 ?v_101))) (= x_94 (or ?v_102 ?v_103))) (= x_92 (or ?v_104 ?v_105))) ?v_106)) ?v_131) ?v_132) ?v_149) ?v_134) ?v_135) ?v_136) (and (and (and (and (and (and (and (or (and (and (and (and (and (and (and (and (and (and (and ?v_89 (or (or (and (and (and ?v_107 ?v_108) ?v_118) ?v_114) (and (and (and ?v_109 ?v_110) ?v_119) ?v_116)) (and (and ?v_99 ?v_120) ?v_117))) ?v_112) (or (or (or (or ?v_113 ?v_125) x_73) x_62) (not (< x_89 x_83)))) (or (or (or (or ?v_115 ?v_126) x_74) x_63) (not (< x_89 x_84)))) (or (or (or ?v_127 x_72) x_61) (not (< x_89 x_86)))) (or (or (or (and (and (and (and ?v_118 ?v_108) ?v_114) ?v_137) ?v_138) (and (and (and (and ?v_119 ?v_110) ?v_116) ?v_139) ?v_140)) (and (and (and (and ?v_120 ?v_99) ?v_117) ?v_141) ?v_142)) (and (< x_76 ?v_128) ?v_121))) (= x_104 (or x_73 ?v_122))) (= x_105 (or x_74 ?v_123))) (= x_103 (or x_72 ?v_124))) ?v_129) ?v_130) (and (and (and (and (and (and (and (and (and ?v_89 (or (or (or ?v_113 x_73) x_62) ?v_125)) (or (or (or ?v_115 x_74) x_63) ?v_126)) (or (or x_72 x_61) ?v_127)) x_106) (= x_89 ?v_128)) ?v_129) ?v_130) ?v_131) ?v_132)) ?v_147) ?v_148) ?v_106) ?v_133) ?v_134) ?v_135) ?v_136)) (and (and (and (and (and (and (and (or (and (and (and (and (and (and (and (and (and (and (and ?v_143 ?v_144) (not x_90)) (or (or (or ?v_113 x_65) x_62) (<= x_89 x_83))) (or (or (or ?v_115 x_66) x_63) (<= x_89 x_84))) (or (or x_64 x_61) (<= x_89 x_86))) (or (or (or (and (and (and (and (not x_65) ?v_108) (< x_58 x_83)) ?v_137) ?v_138) (and (and (and (and (not x_66) ?v_110) (< x_58 x_84)) ?v_139) ?v_140)) (and (and (and (not x_64) ?v_99) ?v_141) ?v_142)) ?v_121)) (= x_96 (or x_65 (= x_83 x_89)))) (= x_97 (or x_66 (= x_84 x_89)))) (= x_95 (or x_64 (= x_86 x_89)))) ?v_145) ?v_146) (and (and (and (and (and (and (and ?v_143 (not ?v_144)) x_90) ?v_145) ?v_146) (= x_89 x_58)) ?v_134) ?v_135)) ?v_147) ?v_148) ?v_106) ?v_133) ?v_131) ?v_132) ?v_149))) (or (or (and ?v_150 (= x_91 (ite (not x_71) x_60 1))) (and ?v_151 (= x_91 (ite ?v_176 x_60 2)))) (and (and (not ?v_150) (not ?v_151)) (= x_91 x_60)))) (or (and (and ?v_152 (not (<= x_107 x_114))) (not (<= x_114 ?v_153))) (and ?v_154 (= x_114 x_83)))) (or (and (and ?v_152 (not (<= x_107 x_115))) (not (<= x_115 ?v_153))) (and ?v_154 (= x_115 x_84)))) (or (and (and ?v_152 (= x_107 (+ x_76 x_10))) x_116) (and (and ?v_154 (not x_116)) (= x_107 x_76)))) (or (and (and (and (and ?v_124 ?v_155) ?v_156) (< x_117 x_118)) (< x_118 x_119)) (and (and (and (not ?v_124) (= x_117 x_86)) (= x_118 x_87)) (= x_119 x_88)))) (or (or (and (and (and (and (and (and (or (and (and (and (and (and (and (and (and (and (and ?v_150 ?v_160) ?v_185) ?v_161) ?v_162) (= x_67 (ite ?v_163 (ite (not (< x_81 3)) 3 x_81) x_36))) (= x_62 ?v_164)) (= x_63 ?v_166)) (= x_61 ?v_168)) ?v_197) ?v_170) (and (and (and (and (and (and (and (and (and (and ?v_150 (not ?v_160)) x_71) (= x_58 x_39)) ?v_161) ?v_162) (= x_67 (ite ?v_163 (ite (not (< x_82 3)) 3 x_82) x_36))) (= x_62 (or ?v_164 ?v_165))) (= x_63 (or ?v_166 ?v_167))) (= x_61 (or ?v_168 ?v_169))) ?v_170)) ?v_195) ?v_196) ?v_213) ?v_198) ?v_199) ?v_200) (and (and (and (and (and (and (and (or (and (and (and (and (and (and (and (and (and (and (and ?v_151 (or (or (and (and (and ?v_171 ?v_172) ?v_182) ?v_178) (and (and (and ?v_173 ?v_174) ?v_183) ?v_180)) (and (and ?v_163 ?v_184) ?v_181))) ?v_176) (or (or (or (or ?v_177 ?v_189) x_42) x_31) (not (< x_58 x_52)))) (or (or (or (or ?v_179 ?v_190) x_43) x_32) (not (< x_58 x_53)))) (or (or (or ?v_191 x_41) x_30) (not (< x_58 x_55)))) (or (or (or (and (and (and (and ?v_182 ?v_172) ?v_178) ?v_201) ?v_202) (and (and (and (and ?v_183 ?v_174) ?v_180) ?v_203) ?v_204)) (and (and (and (and ?v_184 ?v_163) ?v_181) ?v_205) ?v_206)) (and (< x_45 ?v_192) ?v_185))) (= x_73 (or x_42 ?v_186))) (= x_74 (or x_43 ?v_187))) (= x_72 (or x_41 ?v_188))) ?v_193) ?v_194) (and (and (and (and (and (and (and (and (and ?v_151 (or (or (or ?v_177 x_42) x_31) ?v_189)) (or (or (or ?v_179 x_43) x_32) ?v_190)) (or (or x_41 x_30) ?v_191)) x_75) (= x_58 ?v_192)) ?v_193) ?v_194) ?v_195) ?v_196)) ?v_211) ?v_212) ?v_170) ?v_197) ?v_198) ?v_199) ?v_200)) (and (and (and (and (and (and (and (or (and (and (and (and (and (and (and (and (and (and (and ?v_207 ?v_208) (not x_59)) (or (or (or ?v_177 x_34) x_31) (<= x_58 x_52))) (or (or (or ?v_179 x_35) x_32) (<= x_58 x_53))) (or (or x_33 x_30) (<= x_58 x_55))) (or (or (or (and (and (and (and (not x_34) ?v_172) (< x_27 x_52)) ?v_201) ?v_202) (and (and (and (and (not x_35) ?v_174) (< x_27 x_53)) ?v_203) ?v_204)) (and (and (and (not x_33) ?v_163) ?v_205) ?v_206)) ?v_185)) (= x_65 (or x_34 (= x_52 x_58)))) (= x_66 (or x_35 (= x_53 x_58)))) (= x_64 (or x_33 (= x_55 x_58)))) ?v_209) ?v_210) (and (and (and (and (and (and (and ?v_207 (not ?v_208)) x_59) ?v_209) ?v_210) (= x_58 x_27)) ?v_198) ?v_199)) ?v_211) ?v_212) ?v_170) ?v_197) ?v_195) ?v_196) ?v_213))) (or (or (and ?v_214 (= x_60 (ite (not x_40) x_29 1))) (and ?v_215 (= x_60 (ite ?v_243 x_29 2)))) (and (and (not ?v_214) (not ?v_215)) (= x_60 x_29)))) (or (and (and ?v_216 (not (<= x_76 x_83))) (not (<= x_83 ?v_217))) (and ?v_218 (= x_83 x_52)))) (or (and (and ?v_216 (not (<= x_76 x_84))) (not (<= x_84 ?v_217))) (and ?v_218 (= x_84 x_53)))) (or (and (and ?v_216 (= x_76 (+ x_45 x_10))) x_85) (and (and ?v_218 (not x_85)) (= x_76 x_45)))) (or (and (and (and (and ?v_188 ?v_219) ?v_220) (< x_86 x_87)) (< x_87 x_88)) (and (and (and (not ?v_188) (= x_86 x_55)) (= x_87 x_56)) (= x_88 x_57)))) (or (or (and (and (and (and (and (and (or (and (and (and (and (and (and (and (and (and (and ?v_214 ?v_227) ?v_249) ?v_228) ?v_229) (= x_36 (ite ?v_223 (ite (not (< x_50 3)) 3 x_50) x_8))) (= x_31 ?v_230)) (= x_32 ?v_232)) (= x_30 ?v_234)) ?v_261) ?v_236) (and (and (and (and (and (and (and (and (and (and ?v_214 (not ?v_227)) x_40) (= x_27 x_11)) ?v_228) ?v_229) (= x_36 (ite ?v_223 (ite (not (< x_51 3)) 3 x_51) x_8))) (= x_31 (or ?v_230 ?v_231))) (= x_32 (or ?v_232 ?v_233))) (= x_30 (or ?v_234 ?v_235))) ?v_236)) ?v_259) ?v_260) ?v_280) ?v_262) ?v_263) ?v_264) (and (and (and (and (and (and (and (or (and (and (and (and (and (and (and (and (and (and (and ?v_215 (or (or (and (and (and ?v_237 ?v_221) ?v_238) ?v_245) (and (and (and ?v_239 ?v_222) ?v_240) ?v_247)) (and (and ?v_223 ?v_242) ?v_248))) ?v_243) (or (or (or (or ?v_244 ?v_253) x_13) x_3) (not (< x_27 x_21)))) (or (or (or (or ?v_246 ?v_254) x_14) x_4) (not (< x_27 x_22)))) (or (or (or ?v_255 x_15) x_5) (not (< x_27 x_24)))) (or (or (or (and (and (and (and ?v_238 ?v_221) ?v_245) ?v_266) ?v_267) (and (and (and (and ?v_240 ?v_222) ?v_247) ?v_269) ?v_270)) (and (and (and (and ?v_242 ?v_223) ?v_248) ?v_272) ?v_273)) (and (< x_0 ?v_256) ?v_249))) (= x_42 (or x_13 ?v_250))) (= x_43 (or x_14 ?v_251))) (= x_41 (or x_15 ?v_252))) ?v_257) ?v_258) (and (and (and (and (and (and (and (and (and ?v_215 (or (or (or ?v_244 x_13) x_3) ?v_253)) (or (or (or ?v_246 x_14) x_4) ?v_254)) (or (or x_15 x_5) ?v_255)) x_44) (= x_27 ?v_256)) ?v_257) ?v_258) ?v_259) ?v_260)) ?v_278) ?v_279) ?v_236) ?v_261) ?v_262) ?v_263) ?v_264)) (and (and (and (and (and (and (and (or (and (and (and (and (and (and (and (and (and (and (and ?v_274 ?v_275) (not x_28)) (or (or (or ?v_244 x_17) x_3) (<= x_27 x_21))) (or (or (or ?v_246 x_18) x_4) (<= x_27 x_22))) (or (or x_19 x_5) (<= x_27 x_24))) (or (or (or (and (and (and (and ?v_265 ?v_221) (< x_9 x_21)) ?v_266) ?v_267) (and (and (and (and ?v_268 ?v_222) (< x_9 x_22)) ?v_269) ?v_270)) (and (and (and ?v_271 ?v_223) ?v_272) ?v_273)) ?v_249)) (= x_34 (or x_17 (= x_21 x_27)))) (= x_35 (or x_18 (= x_22 x_27)))) (= x_33 (or x_19 (= x_24 x_27)))) ?v_276) ?v_277) (and (and (and (and (and (and (and ?v_274 (not ?v_275)) x_28) ?v_276) ?v_277) (= x_27 x_9)) ?v_262) ?v_263)) ?v_278) ?v_279) ?v_236) ?v_261) ?v_259) ?v_260) ?v_280))) (or (or (and ?v_281 (= x_29 (ite ?v_282 x_20 1))) (and ?v_283 (= x_29 (ite (not x_12) x_20 2)))) (and (and (not ?v_281) (not ?v_283)) (= x_29 x_20)))) (or (and (and ?v_284 (not (<= x_45 x_52))) (not (<= x_52 ?v_285))) (and ?v_286 (= x_52 x_21)))) (or (and (and ?v_284 (not (<= x_45 x_53))) (not (<= x_53 ?v_285))) (and ?v_286 (= x_53 x_22)))) (or (and (and ?v_284 (= x_45 (+ x_0 x_10))) x_54) (and (and ?v_286 (not x_54)) (= x_45 x_0)))) (or (and (and (and (and ?v_252 ?v_287) ?v_288) (< x_55 x_56)) (< x_56 x_57)) (and (and (and (not ?v_252) (= x_55 x_24)) (= x_56 x_25)) (= x_57 x_26)))) (or (or (or (or (or (or (or (or (or (not (<= x_130 2)) (not (<= x_131 2))) (not (<= x_99 2))) (not (<= x_100 2))) (not (<= x_68 2))) (not (<= x_69 2))) (not (<= x_37 2))) (not (<= x_38 2))) (not (<= x_6 2))) (not (<= x_7 2)))))))))))))))))))))))))))))))))))
(check-sat)
(exit)
